Example 7 in [Borralleras, Lucas & Rubio - CADE'02]

(Subsumes [Luc96a, Example 3.12] and [Luc02b, Example 1])

Summary: Ex7_BLR02

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)
• Positive results:
  1. Zantema's transformation (RPOS @ AProVE)
  2. Ferreira and Ribeiro's transformation (Corollary)
  3. Giesl and Middeldorp's transformation (Corollary)
  4. CSRPO
  5. Polynomial interpretation

CS-TRS Ex7_BLR02 (file Ex7_BLR02.csr)

Showing the CS-TRS  Ex7_BLR02:


Functions:  from cons s head 2nd take 0 nil sel

Constructors:  cons s 0 nil

Variables:  X XS N

Arities: 

ar(from) = 1
ar(cons) = 2
ar(s) = 1
ar(head) = 1
ar(2nd) = 1
ar(take) = 2
ar(0) = 0
ar(nil) = 0
ar(sel) = 2

Replacement map: 

µ(from)={1}(cons,[1])
µ(cons)={1}
µ(s)={1}
µ(head)={1}
µ(2nd)={1}
µ(take)={1,2}
µ(0)={}
µ(nil)={}
µ(sel)={1,2}

Rules: (file Ex7_BLR02) 

from(X) -> cons(X,from(s(X)))
head(cons(X,XS)) -> X
2nd(cons(X,XS)) -> head(XS)
take(0,XS) -> nil
take(s(N),cons(X,XS)) -> cons(X,take(N,XS))
sel(0,cons(X,XS)) -> X
sel(s(N),cons(X,XS)) -> sel(N,XS)

The CS-TRS in OBJ format (file Ex7_BLR02.obj):

obj Ex7_BLR02 is
  sort S .
  op from : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op head : S -> S .
  op 2nd : S -> S .
  op take : S S -> S .
  op 0 : -> S .
  op nil : -> S .
  op sel : S S -> S .
  vars X XS N : S .
  eq from(X) = cons(X,from(s(X))) .
  eq head(cons(X,XS)) = X .
  eq 2nd(cons(X,XS)) = head(XS) .
  eq take(0,XS) = nil .
  eq take(s(N),cons(X,XS)) = cons(X,take(N,XS)) .
  eq sel(0,cons(X,XS)) = X .
  eq sel(s(N),cons(X,XS)) = sel(N,XS) .
endo

Negative results

1. The µ-termination of Ex7_BLR02 cannot be proved by using Lucas' transformation. The TRS Ex7_BLR02_L:

       from(X) -> cons(X)
       head(cons(X)) -> X
       2nd(cons(X)) -> head(XS)
       take(0,XS) -> nil
       take(s(N),cons(X)) -> cons(X)
       sel(0,cons(X)) -> X
       sel(s(X),cons(Y)) -> sel(X,Z)
       

   contains extra variables.

Positive results

1. The µ-termination of Ex7_BLR02 can be proved by using Zantema's transformation. The TRS Ex7_BLR02_Z:

       from(X) -> cons(X,n__from(s(X)))
       head(cons(X,XS)) -> X
       2nd(cons(X,XS)) -> head(activate(XS))
       take(0,XS) -> nil
       take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
       sel(0,cons(X,XS)) -> X
       sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
       from(X) -> n__from(X)
       take(X1,X2) -> n__take(X1,X2)
       activate(n__from(X)) -> from(X)
       activate(n__take(X1,X2)) -> take(X1,X2)
       activate(X) -> X
       

   is terminating (use RPOS with AProVE).
2. By [GM04, Theorem 11], the µ-termination of Ex1_Luc02b can also be proved by using Ferreira and Ribeiro's transformation (but no concrete proof has been reported yet).
3. By [GM04, Theorem 22], the µ-termination of Ex1_Luc02b can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).
4. The µ-termination of Ex7_BLR02 can be proved by CSRPO together with the following [BLR02, Example 7] and automatically computed by MuTerm:
   • marking map:

            m(cons,2)=m(_cons,2)={from}
            

   • precedence:

            2nd > head, from
            take > from, nil, cons
            sel > from > cons, s, _from
            

   • status:

            st(take)=st(sel)=lex; 
            st(f)=mul for all other symbols f.
            

5. The µ-termination of Ex7_BLR02 can be proved by using a polynomial interpretation over Q_1:

      [from](x) = 2x + 4
      [cons](x,y) = x + y/4
      [s](x) = 2x + 2
      [head](x) = x + 1
      [2nd](x) = 4x + 2
      [take](x,y) = x + y + 1
      [0] = 0
      [nil] = 0
      [sel](x,y) = (x^2)y + x + y + 1